Правило резолюций

Система логического вывода, оперирующая клозами — элементарными дизъюнкциями, которые рассматриваются как множества литералов (порядок не важен, повторения исключаются). Аксиомы отсутствуют, исходными условиями являются все клозы КНФ, а целью работы — получение пустого клоза $\square$.

Если существуют клозы вида $x \lor C$ и $\bar{x} \lor D$, где $x$ — переменная, то выводится новый клоз $C \lor D$. Если $C$ и $D$ являются пустыми множествами, результатом вывода становится пустой клоз $\square$. Клоз, содержащий пару литералов $\{y, \bar{y}\}$, в результат не записывается.

Доказать утверждение: $((I \to A) \land (S \to I) \land ((\bar{S} \land \bar{I}) \to F) \land \bar{A}) \to F$ Где $I$ — invite, $A$ — attend, $S$ — see, $F$ — fire.

Для доказательства составим КНФ отрицания теоремы (множество клозов): $$S = \{ \bar{I} \lor A,~~ \bar{S} \lor I,~~ S \lor I \lor F,~~ \bar{A},~~ \bar{F} \}$$ Выполним последовательный вывод пустого клоза: $$\begin{matrix} 1. & S \lor I \lor F & \text{условие} \\ 2. & \bar{F} & \text{условие} \\ 3. & S \lor I & \text{рез. 1, 2} \\ 4. & \bar{S} \lor I & \text{условие} \\ 5. & I & \text{рез. 3, 4} \\ 6. & \bar{I} \lor A & \text{условие} \\ 7. & A & \text{рез. 5, 6} \\ 8. & \bar{A} & \text{условие} \\ 9. & \square & \text{рез. 7, 8} \end{matrix}$$ $\square$